import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

/**
 * 
 * @author "Cunxin Jia"
 *
 */
public class LGG {
	
	/**
	 * Generate LGG of clauses
	 * @param clause1
	 * @param clause2
	 * @return the LGG clause
	 */
	public static Clause generateLGG(Clause clause1, Clause clause2) {
		if(clause1 == null || clause2 == null) {
			return null;
		}
		Literal head = generateLGG(clause1.getHead(), clause2.getHead());
		if(head == null) {
			return null;
		}
		Set<Literal> body1 = clause1.getBody();
		Set<Literal> body2 = clause2.getBody();
		Set<Literal> body = new HashSet<Literal> ();
		Object[] bodyArray1 = body1.toArray();
		Object[] bodyArray2 = body2.toArray();
		for(int i = 0; i < bodyArray1.length; i++) {
			for(int j = 0; j < bodyArray2.length; j++) {
				Literal literal_i = (Literal) bodyArray1[i];
				Literal literal_j = (Literal) bodyArray2[j];
				Literal lggLiteral = generateLGG(literal_i, literal_j);
				if(lggLiteral != null) {
					body.add(lggLiteral);
				}
			}
		}
		Clause lggClause = new Clause(head, body);		
		return lggClause;
	}
	
	/**
	 * Generate LGG of literals
	 * @param literal1
	 * @param literal2
	 * @return the LGG literal
	 */
	public static Literal generateLGG(Literal literal1, Literal literal2) {
		if(literal1 == null || literal2 == null) {
			return null;
		}
		if(literal1.isNegative() && literal2.isPositive() ||
				literal2.isNegative() && literal1.isPositive() ||
				literal1.equals(literal2)) {
			return null;
		}
		else {
			Atom lggAtom = generateLGG(literal1.getAtom(), literal2.getAtom());
			if(lggAtom == null)
				return null;
			Literal lggLiteral = new Literal(lggAtom, literal1.isNegative());
			return lggLiteral;
		}
	}
	
	/**
	 * Generate LGG of atoms
	 * @param atom1
	 * @param atom2
	 * @return the LGG atom
	 */
	public static Atom generateLGG(Atom atom1, Atom atom2) {
		if(!atom1.getPredicate().equals(atom2.getPredicate())  || 
				atom1.getTerms().size() != atom2.getTerms().size()) {
			return null;
		}
		else {
			List<Term> terms1 = atom1.getTerms();
			List<Term> terms2 = atom2.getTerms();
			List<Term> lggTerms = new ArrayList<Term>();
			for(int i = 0; i < terms1.size(); i++) {
				Term lggTerm = generateLGG(terms1.get(i), terms2.get(i));
				lggTerms.add(lggTerm);
			}
			Atom lggAtom = new Atom(atom1.getPredicate(),lggTerms);
			return lggAtom;
		}		
	}
	
	/**
	 * Generate LGG of terms
	 * @param term1
	 * @param term2
	 * @return the LGG term
	 */	
	public static Term generateLGG(Term term1, Term term2) {
		if(term1.equals(term2)) {
			return term1;
		}
		else {
			String newVar = VarFactory.getInstance().getLGGTerm(term1, term2);
			Term lggTerm = new Term(newVar);
			return lggTerm;
		}
	}
	
	
	/**
	 * remove redundant literals
	 * @param clause
	 * @return
	 */
	public static Clause reduceClause(Clause clause) {
		Set<Term> necessaryTerms = new HashSet<Term> ();
		necessaryTerms.addAll(clause.getHead().getAtom().getTerms());
		int formerSize = 0;
		while(necessaryTerms.size() > formerSize) {
			formerSize = necessaryTerms.size();
			Set<Literal> body = clause.getBody();
			Iterator<Literal> iter = body.iterator();
			while(iter.hasNext()) {
				Literal curLiteral = iter.next();
				List<Term> terms = curLiteral.getAtom().getTerms();
				for(Term term:terms) {
					if(necessaryTerms.contains(term)) {
						necessaryTerms.addAll(terms);
						break;
					}
				}
			}
		}
		
		Clause reduced = clause;		
		Iterator<Literal> iter = reduced.getBody().iterator();
		while(iter.hasNext()) {
			List<Term> terms = iter.next().getAtom().getTerms();
			if(!necessaryTerms.containsAll(terms)) {
				iter.remove();
			}
		}
		return reduced;
	}
}
